M.rframe(A.pre p for a)
== xdom(1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M)))))))))))). 

== L=1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M)))))))))))(x)  
== Ldeq-member(KindDeq;locl(a);L)
==  (s1, s2:A.state, v:A.da(locl(a)). (s1  s2 mod x)  (p(s1,v)  p(s2,v))) 

latex

---

clarification:

M.rframe(A.pre p for a)
== fpf-all(Id;
== fpf-all(IdDeq;
== fpf-all(1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M)))))))))));
== fpf-all(x,L.(deq-member(KindDeq;locl(a);L)
== fpf-all( (s1:A.state, s2:A.state, v:A.da(locl(a)).
== fpf-all( (ma-x-equiv(A;x;s1;s2)  (p(s1,v)  p(s2,v))))) 

latex

Definitions	xdom(f). v=f(x)   P(x;v), Id, IdDeq, 1of(t), 2of(t), P  Q, b, deq-member(eq;x;L), KindDeq, M.state, x:A. B(x), M.da(a), locl(a), P  Q, (s1  s2 mod x), P  Q, f(a)
FDL editor aliases	ma-rframe-pre